'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ i^#(0(x1)) -> c_0(p^#(s(p(s(0(p(s(p(s(x1))))))))))
, i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))
, j^#(0(x1)) -> c_2(p^#(s(p(p(s(s(0(p(s(p(s(x1))))))))))))
, j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))
, p^#(s(x1)) -> c_5()
, p^#(0(x1)) -> c_6()}
The usable rules are:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
The estimated dependency graph contains the following edges:
{i^#(0(x1)) -> c_0(p^#(s(p(s(0(p(s(p(s(x1))))))))))}
==> {p^#(s(x1)) -> c_5()}
{i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))}
==> {p^#(s(x1)) -> c_5()}
{j^#(0(x1)) -> c_2(p^#(s(p(p(s(s(0(p(s(p(s(x1))))))))))))}
==> {p^#(s(x1)) -> c_5()}
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
==> {p^#(p(s(x1))) -> c_4(p^#(x1))}
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
==> {p^#(0(x1)) -> c_6()}
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
==> {p^#(s(x1)) -> c_5()}
{p^#(p(s(x1))) -> c_4(p^#(x1))}
==> {p^#(0(x1)) -> c_6()}
{p^#(p(s(x1))) -> c_4(p^#(x1))}
==> {p^#(s(x1)) -> c_5()}
{p^#(p(s(x1))) -> c_4(p^#(x1))}
==> {p^#(p(s(x1))) -> c_4(p^#(x1))}
We consider the following path(s):
1) { i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))
, p^#(s(x1)) -> c_5()}
The usable rules for this path are the following:
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))
, p^#(s(x1)) -> c_5()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_5()}
and weakly orienting the rules
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_5()}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [8]
i^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [2]
c_1(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))}
and weakly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_5()
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [8]
i^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
and weakly orienting the rules
{ i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_5()
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [4]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [8]
i^#(x1) = [1] x1 + [15]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_5()
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_5()
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ i_0(21) -> 60
, i_0(21) -> 64
, i_1(87) -> 97
, i_1(87) -> 101
, i_2(127) -> 122
, i_2(127) -> 126
, i_2(138) -> 133
, i_2(138) -> 137
, i_2(208) -> 203
, i_2(208) -> 207
, i_2(219) -> 214
, i_2(219) -> 218
, i_2(289) -> 284
, i_2(289) -> 288
, i_2(300) -> 295
, i_2(300) -> 299
, i_2(370) -> 365
, i_2(370) -> 369
, i_2(381) -> 376
, i_2(381) -> 380
, 0_0(2) -> 2
, 0_0(2) -> 15
, 0_0(2) -> 17
, 0_0(2) -> 19
, 0_0(2) -> 20
, 0_0(2) -> 21
, 0_0(2) -> 22
, 0_0(2) -> 70
, 0_0(2) -> 72
, 0_0(2) -> 74
, 0_0(2) -> 87
, 0_0(2) -> 89
, 0_0(2) -> 381
, 0_0(2) -> 383
, 0_0(2) -> 391
, 0_0(2) -> 393
, 0_0(2) -> 395
, 0_0(4) -> 2
, 0_0(4) -> 15
, 0_0(4) -> 17
, 0_0(4) -> 19
, 0_0(4) -> 20
, 0_0(4) -> 21
, 0_0(4) -> 22
, 0_0(4) -> 70
, 0_0(4) -> 72
, 0_0(4) -> 74
, 0_0(4) -> 87
, 0_0(4) -> 89
, 0_0(4) -> 381
, 0_0(4) -> 383
, 0_0(4) -> 391
, 0_0(4) -> 393
, 0_0(4) -> 395
, 0_0(21) -> 14
, 0_0(21) -> 52
, 0_0(21) -> 56
, 0_0(22) -> 20
, 0_1(82) -> 15
, 0_1(82) -> 17
, 0_1(82) -> 19
, 0_1(82) -> 20
, 0_1(82) -> 21
, 0_1(87) -> 14
, 0_1(87) -> 60
, 0_1(87) -> 64
, 0_1(87) -> 66
, 0_1(87) -> 68
, 0_1(87) -> 69
, 0_1(87) -> 91
, 0_1(87) -> 97
, 0_1(87) -> 101
, 0_1(87) -> 376
, 0_1(87) -> 380
, 0_1(87) -> 389
, 0_2(413) -> 376
, 0_2(413) -> 380
, 0_2(413) -> 389
, p_0(2) -> 15
, p_0(2) -> 17
, p_0(2) -> 19
, p_0(2) -> 20
, p_0(2) -> 21
, p_0(4) -> 15
, p_0(4) -> 17
, p_0(4) -> 19
, p_0(4) -> 20
, p_0(4) -> 21
, p_0(4) -> 22
, p_0(4) -> 70
, p_0(4) -> 72
, p_0(4) -> 74
, p_0(4) -> 87
, p_0(4) -> 89
, p_0(4) -> 381
, p_0(4) -> 383
, p_0(4) -> 391
, p_0(4) -> 393
, p_0(4) -> 395
, p_0(12) -> 11
, p_0(16) -> 15
, p_0(18) -> 15
, p_0(18) -> 17
, p_0(20) -> 15
, p_0(20) -> 17
, p_0(20) -> 19
, p_0(21) -> 20
, p_0(22) -> 15
, p_0(22) -> 17
, p_0(22) -> 19
, p_0(22) -> 20
, p_0(22) -> 21
, p_0(51) -> 14
, p_0(53) -> 14
, p_0(53) -> 52
, p_0(54) -> 53
, p_0(55) -> 14
, p_0(55) -> 52
, p_0(61) -> 60
, p_0(62) -> 61
, p_0(63) -> 60
, p_1(65) -> 60
, p_1(65) -> 64
, p_1(67) -> 14
, p_1(67) -> 60
, p_1(67) -> 64
, p_1(67) -> 66
, p_1(67) -> 69
, p_1(67) -> 91
, p_1(67) -> 97
, p_1(67) -> 101
, p_1(67) -> 376
, p_1(67) -> 380
, p_1(67) -> 389
, p_1(68) -> 376
, p_1(68) -> 380
, p_1(68) -> 389
, p_1(69) -> 389
, p_1(71) -> 70
, p_1(73) -> 70
, p_1(73) -> 72
, p_1(75) -> 70
, p_1(75) -> 72
, p_1(75) -> 74
, p_1(76) -> 75
, p_1(77) -> 76
, p_1(78) -> 77
, p_1(79) -> 76
, p_1(80) -> 75
, p_1(81) -> 70
, p_1(81) -> 72
, p_1(81) -> 74
, p_1(81) -> 87
, p_1(81) -> 89
, p_1(88) -> 87
, p_1(90) -> 14
, p_1(90) -> 69
, p_1(90) -> 97
, p_1(90) -> 101
, p_1(90) -> 376
, p_1(90) -> 380
, p_1(90) -> 389
, p_1(91) -> 376
, p_1(91) -> 380
, p_1(91) -> 389
, p_1(92) -> 14
, p_1(92) -> 69
, p_1(92) -> 91
, p_1(92) -> 97
, p_1(92) -> 101
, p_1(92) -> 376
, p_1(92) -> 380
, p_1(92) -> 389
, p_1(93) -> 92
, p_1(96) -> 97
, p_1(96) -> 101
, p_1(97) -> 376
, p_1(97) -> 380
, p_1(98) -> 97
, p_1(98) -> 101
, p_1(99) -> 98
, p_1(100) -> 97
, p_1(100) -> 101
, p_1(101) -> 376
, p_1(101) -> 380
, p_1(380) -> 389
, p_2(68) -> 389
, p_2(69) -> 389
, p_2(91) -> 389
, p_2(102) -> 97
, p_2(102) -> 101
, p_2(102) -> 376
, p_2(102) -> 380
, p_2(103) -> 376
, p_2(103) -> 380
, p_2(103) -> 389
, p_2(104) -> 97
, p_2(104) -> 101
, p_2(104) -> 103
, p_2(104) -> 376
, p_2(104) -> 380
, p_2(105) -> 376
, p_2(105) -> 380
, p_2(105) -> 389
, p_2(106) -> 389
, p_2(108) -> 107
, p_2(110) -> 107
, p_2(110) -> 109
, p_2(112) -> 107
, p_2(112) -> 109
, p_2(112) -> 111
, p_2(113) -> 112
, p_2(114) -> 113
, p_2(115) -> 114
, p_2(116) -> 113
, p_2(117) -> 112
, p_2(118) -> 107
, p_2(118) -> 109
, p_2(118) -> 111
, p_2(118) -> 127
, p_2(118) -> 129
, p_2(123) -> 122
, p_2(124) -> 123
, p_2(125) -> 122
, p_2(125) -> 126
, p_2(128) -> 127
, p_2(134) -> 133
, p_2(135) -> 134
, p_2(136) -> 133
, p_2(136) -> 137
, p_2(139) -> 138
, p_2(141) -> 138
, p_2(141) -> 140
, p_2(141) -> 148
, p_2(141) -> 150
, p_2(141) -> 152
, p_2(142) -> 122
, p_2(142) -> 126
, p_2(149) -> 148
, p_2(151) -> 148
, p_2(151) -> 150
, p_2(153) -> 148
, p_2(153) -> 150
, p_2(153) -> 152
, p_2(154) -> 153
, p_2(155) -> 154
, p_2(156) -> 155
, p_2(157) -> 154
, p_2(158) -> 153
, p_2(170) -> 133
, p_2(170) -> 137
, p_2(177) -> 176
, p_2(179) -> 176
, p_2(179) -> 178
, p_2(181) -> 176
, p_2(181) -> 178
, p_2(181) -> 180
, p_2(182) -> 181
, p_2(183) -> 182
, p_2(184) -> 183
, p_2(185) -> 182
, p_2(186) -> 181
, p_2(187) -> 176
, p_2(187) -> 178
, p_2(187) -> 180
, p_2(187) -> 208
, p_2(187) -> 210
, p_2(204) -> 203
, p_2(205) -> 204
, p_2(206) -> 203
, p_2(206) -> 207
, p_2(209) -> 208
, p_2(215) -> 214
, p_2(216) -> 215
, p_2(217) -> 214
, p_2(217) -> 218
, p_2(220) -> 219
, p_2(222) -> 219
, p_2(222) -> 221
, p_2(222) -> 229
, p_2(222) -> 231
, p_2(222) -> 233
, p_2(223) -> 203
, p_2(223) -> 207
, p_2(230) -> 229
, p_2(232) -> 229
, p_2(232) -> 231
, p_2(234) -> 229
, p_2(234) -> 231
, p_2(234) -> 233
, p_2(235) -> 234
, p_2(236) -> 235
, p_2(237) -> 236
, p_2(238) -> 235
, p_2(239) -> 234
, p_2(251) -> 214
, p_2(251) -> 218
, p_2(258) -> 257
, p_2(260) -> 257
, p_2(260) -> 259
, p_2(262) -> 257
, p_2(262) -> 259
, p_2(262) -> 261
, p_2(263) -> 262
, p_2(264) -> 263
, p_2(265) -> 264
, p_2(266) -> 263
, p_2(267) -> 262
, p_2(268) -> 257
, p_2(268) -> 259
, p_2(268) -> 261
, p_2(268) -> 289
, p_2(268) -> 291
, p_2(285) -> 284
, p_2(286) -> 285
, p_2(287) -> 284
, p_2(287) -> 288
, p_2(290) -> 289
, p_2(296) -> 295
, p_2(297) -> 296
, p_2(298) -> 295
, p_2(298) -> 299
, p_2(301) -> 300
, p_2(303) -> 300
, p_2(303) -> 302
, p_2(303) -> 310
, p_2(303) -> 312
, p_2(303) -> 314
, p_2(304) -> 284
, p_2(304) -> 288
, p_2(311) -> 310
, p_2(313) -> 310
, p_2(313) -> 312
, p_2(315) -> 310
, p_2(315) -> 312
, p_2(315) -> 314
, p_2(316) -> 315
, p_2(317) -> 316
, p_2(318) -> 317
, p_2(319) -> 316
, p_2(320) -> 315
, p_2(332) -> 295
, p_2(332) -> 299
, p_2(339) -> 338
, p_2(341) -> 338
, p_2(341) -> 340
, p_2(343) -> 338
, p_2(343) -> 340
, p_2(343) -> 342
, p_2(344) -> 343
, p_2(345) -> 344
, p_2(346) -> 345
, p_2(347) -> 344
, p_2(348) -> 343
, p_2(349) -> 338
, p_2(349) -> 340
, p_2(349) -> 342
, p_2(349) -> 370
, p_2(349) -> 372
, p_2(366) -> 365
, p_2(367) -> 366
, p_2(368) -> 365
, p_2(368) -> 369
, p_2(371) -> 370
, p_2(375) -> 376
, p_2(375) -> 380
, p_2(376) -> 389
, p_2(377) -> 376
, p_2(377) -> 380
, p_2(378) -> 377
, p_2(379) -> 376
, p_2(379) -> 380
, p_2(380) -> 389
, p_2(382) -> 381
, p_2(384) -> 381
, p_2(384) -> 383
, p_2(384) -> 391
, p_2(384) -> 393
, p_2(384) -> 395
, p_2(385) -> 365
, p_2(385) -> 369
, p_2(392) -> 391
, p_2(394) -> 391
, p_2(394) -> 393
, p_2(396) -> 391
, p_2(396) -> 393
, p_2(396) -> 395
, p_2(397) -> 396
, p_2(398) -> 397
, p_2(399) -> 398
, p_2(400) -> 397
, p_2(401) -> 396
, s_0(2) -> 4
, s_0(2) -> 15
, s_0(2) -> 17
, s_0(2) -> 19
, s_0(2) -> 20
, s_0(2) -> 21
, s_0(2) -> 22
, s_0(2) -> 70
, s_0(2) -> 72
, s_0(2) -> 74
, s_0(2) -> 87
, s_0(2) -> 89
, s_0(2) -> 381
, s_0(2) -> 383
, s_0(2) -> 391
, s_0(2) -> 393
, s_0(2) -> 395
, s_0(4) -> 4
, s_0(4) -> 15
, s_0(4) -> 17
, s_0(4) -> 19
, s_0(4) -> 20
, s_0(4) -> 21
, s_0(4) -> 22
, s_0(4) -> 70
, s_0(4) -> 72
, s_0(4) -> 74
, s_0(4) -> 87
, s_0(4) -> 89
, s_0(4) -> 381
, s_0(4) -> 383
, s_0(4) -> 391
, s_0(4) -> 393
, s_0(4) -> 395
, s_0(11) -> 10
, s_0(13) -> 12
, s_0(14) -> 11
, s_0(14) -> 13
, s_0(17) -> 16
, s_0(19) -> 18
, s_0(22) -> 2
, s_0(22) -> 15
, s_0(22) -> 17
, s_0(22) -> 19
, s_0(22) -> 20
, s_0(22) -> 21
, s_0(22) -> 22
, s_0(22) -> 70
, s_0(22) -> 72
, s_0(22) -> 74
, s_0(22) -> 87
, s_0(22) -> 89
, s_0(22) -> 381
, s_0(22) -> 383
, s_0(22) -> 391
, s_0(22) -> 393
, s_0(22) -> 395
, s_0(52) -> 51
, s_0(55) -> 54
, s_0(56) -> 53
, s_0(56) -> 55
, s_0(57) -> 14
, s_0(58) -> 57
, s_0(59) -> 58
, s_0(60) -> 59
, s_0(63) -> 62
, s_0(64) -> 61
, s_0(64) -> 63
, s_1(2) -> 75
, s_1(2) -> 81
, s_1(2) -> 338
, s_1(2) -> 340
, s_1(2) -> 342
, s_1(2) -> 370
, s_1(2) -> 372
, s_1(4) -> 75
, s_1(4) -> 81
, s_1(4) -> 338
, s_1(4) -> 340
, s_1(4) -> 342
, s_1(4) -> 370
, s_1(4) -> 372
, s_1(22) -> 75
, s_1(22) -> 81
, s_1(22) -> 338
, s_1(22) -> 340
, s_1(22) -> 342
, s_1(22) -> 370
, s_1(22) -> 372
, s_1(66) -> 65
, s_1(67) -> 93
, s_1(68) -> 67
, s_1(68) -> 92
, s_1(69) -> 14
, s_1(69) -> 60
, s_1(69) -> 64
, s_1(69) -> 66
, s_1(69) -> 68
, s_1(69) -> 69
, s_1(69) -> 91
, s_1(69) -> 97
, s_1(69) -> 101
, s_1(69) -> 376
, s_1(69) -> 380
, s_1(69) -> 389
, s_1(72) -> 71
, s_1(74) -> 73
, s_1(78) -> 85
, s_1(78) -> 176
, s_1(78) -> 178
, s_1(78) -> 180
, s_1(78) -> 208
, s_1(78) -> 210
, s_1(79) -> 78
, s_1(79) -> 219
, s_1(79) -> 221
, s_1(79) -> 229
, s_1(79) -> 231
, s_1(79) -> 233
, s_1(80) -> 77
, s_1(80) -> 79
, s_1(80) -> 257
, s_1(80) -> 259
, s_1(80) -> 261
, s_1(80) -> 289
, s_1(80) -> 291
, s_1(81) -> 76
, s_1(81) -> 80
, s_1(81) -> 300
, s_1(81) -> 302
, s_1(81) -> 310
, s_1(81) -> 312
, s_1(81) -> 314
, s_1(82) -> 75
, s_1(82) -> 81
, s_1(82) -> 338
, s_1(82) -> 340
, s_1(82) -> 342
, s_1(82) -> 370
, s_1(82) -> 372
, s_1(83) -> 70
, s_1(83) -> 72
, s_1(83) -> 74
, s_1(83) -> 82
, s_1(83) -> 87
, s_1(83) -> 89
, s_1(83) -> 381
, s_1(83) -> 383
, s_1(83) -> 391
, s_1(83) -> 393
, s_1(83) -> 395
, s_1(84) -> 83
, s_1(84) -> 107
, s_1(84) -> 109
, s_1(84) -> 111
, s_1(84) -> 127
, s_1(84) -> 129
, s_1(85) -> 84
, s_1(85) -> 138
, s_1(85) -> 140
, s_1(85) -> 148
, s_1(85) -> 150
, s_1(85) -> 152
, s_1(89) -> 88
, s_1(91) -> 90
, s_1(94) -> 14
, s_1(94) -> 69
, s_1(94) -> 376
, s_1(94) -> 380
, s_1(94) -> 389
, s_1(95) -> 94
, s_1(95) -> 389
, s_1(96) -> 95
, s_1(97) -> 96
, s_1(100) -> 99
, s_1(101) -> 98
, s_1(101) -> 100
, s_2(2) -> 384
, s_2(2) -> 396
, s_2(4) -> 384
, s_2(4) -> 396
, s_2(22) -> 384
, s_2(22) -> 396
, s_2(78) -> 222
, s_2(78) -> 234
, s_2(79) -> 262
, s_2(79) -> 268
, s_2(80) -> 303
, s_2(80) -> 315
, s_2(81) -> 343
, s_2(81) -> 349
, s_2(82) -> 384
, s_2(82) -> 396
, s_2(83) -> 112
, s_2(83) -> 118
, s_2(84) -> 141
, s_2(84) -> 153
, s_2(85) -> 181
, s_2(85) -> 187
, s_2(87) -> 420
, s_2(103) -> 102
, s_2(105) -> 104
, s_2(106) -> 97
, s_2(106) -> 101
, s_2(106) -> 103
, s_2(106) -> 105
, s_2(106) -> 376
, s_2(106) -> 380
, s_2(109) -> 108
, s_2(111) -> 110
, s_2(116) -> 115
, s_2(117) -> 114
, s_2(117) -> 116
, s_2(118) -> 113
, s_2(118) -> 117
, s_2(119) -> 69
, s_2(119) -> 376
, s_2(119) -> 380
, s_2(119) -> 389
, s_2(120) -> 119
, s_2(120) -> 389
, s_2(121) -> 120
, s_2(122) -> 121
, s_2(125) -> 124
, s_2(126) -> 123
, s_2(126) -> 125
, s_2(129) -> 128
, s_2(130) -> 106
, s_2(130) -> 376
, s_2(130) -> 380
, s_2(130) -> 389
, s_2(131) -> 130
, s_2(131) -> 389
, s_2(132) -> 131
, s_2(133) -> 132
, s_2(136) -> 135
, s_2(137) -> 134
, s_2(137) -> 136
, s_2(140) -> 139
, s_2(141) -> 154
, s_2(141) -> 158
, s_2(144) -> 142
, s_2(146) -> 122
, s_2(146) -> 126
, s_2(146) -> 144
, s_2(150) -> 149
, s_2(152) -> 151
, s_2(157) -> 156
, s_2(158) -> 155
, s_2(158) -> 157
, s_2(172) -> 170
, s_2(174) -> 133
, s_2(174) -> 137
, s_2(174) -> 172
, s_2(178) -> 177
, s_2(180) -> 179
, s_2(185) -> 184
, s_2(186) -> 183
, s_2(186) -> 185
, s_2(187) -> 182
, s_2(187) -> 186
, s_2(200) -> 146
, s_2(201) -> 200
, s_2(202) -> 201
, s_2(203) -> 202
, s_2(206) -> 205
, s_2(207) -> 204
, s_2(207) -> 206
, s_2(210) -> 209
, s_2(211) -> 174
, s_2(212) -> 211
, s_2(213) -> 212
, s_2(214) -> 213
, s_2(217) -> 216
, s_2(218) -> 215
, s_2(218) -> 217
, s_2(221) -> 220
, s_2(222) -> 235
, s_2(222) -> 239
, s_2(225) -> 223
, s_2(227) -> 203
, s_2(227) -> 207
, s_2(227) -> 225
, s_2(231) -> 230
, s_2(233) -> 232
, s_2(238) -> 237
, s_2(239) -> 236
, s_2(239) -> 238
, s_2(253) -> 251
, s_2(255) -> 214
, s_2(255) -> 218
, s_2(255) -> 253
, s_2(259) -> 258
, s_2(261) -> 260
, s_2(266) -> 265
, s_2(267) -> 264
, s_2(267) -> 266
, s_2(268) -> 263
, s_2(268) -> 267
, s_2(281) -> 227
, s_2(282) -> 281
, s_2(283) -> 282
, s_2(284) -> 283
, s_2(287) -> 286
, s_2(288) -> 285
, s_2(288) -> 287
, s_2(291) -> 290
, s_2(292) -> 255
, s_2(293) -> 292
, s_2(294) -> 293
, s_2(295) -> 294
, s_2(298) -> 297
, s_2(299) -> 296
, s_2(299) -> 298
, s_2(302) -> 301
, s_2(303) -> 316
, s_2(303) -> 320
, s_2(306) -> 304
, s_2(308) -> 284
, s_2(308) -> 288
, s_2(308) -> 306
, s_2(312) -> 311
, s_2(314) -> 313
, s_2(319) -> 318
, s_2(320) -> 317
, s_2(320) -> 319
, s_2(334) -> 332
, s_2(336) -> 295
, s_2(336) -> 299
, s_2(336) -> 334
, s_2(340) -> 339
, s_2(342) -> 341
, s_2(347) -> 346
, s_2(348) -> 345
, s_2(348) -> 347
, s_2(349) -> 344
, s_2(349) -> 348
, s_2(362) -> 308
, s_2(363) -> 362
, s_2(364) -> 363
, s_2(365) -> 364
, s_2(368) -> 367
, s_2(369) -> 366
, s_2(369) -> 368
, s_2(372) -> 371
, s_2(373) -> 336
, s_2(374) -> 373
, s_2(375) -> 374
, s_2(376) -> 375
, s_2(379) -> 378
, s_2(380) -> 377
, s_2(380) -> 379
, s_2(383) -> 382
, s_2(384) -> 397
, s_2(384) -> 401
, s_2(387) -> 385
, s_2(389) -> 365
, s_2(389) -> 369
, s_2(389) -> 387
, s_2(393) -> 392
, s_2(395) -> 394
, s_2(400) -> 399
, s_2(401) -> 398
, s_2(401) -> 400
, s_2(413) -> 420
, s_2(414) -> 413
, s_2(415) -> 414
, s_2(416) -> 415
, s_2(417) -> 416
, s_2(418) -> 417
, s_2(419) -> 418
, s_2(420) -> 419
, j_0(15) -> 14
, j_1(70) -> 69
, j_1(70) -> 376
, j_1(70) -> 380
, j_1(70) -> 389
, j_2(107) -> 106
, j_2(107) -> 376
, j_2(107) -> 380
, j_2(107) -> 389
, j_2(148) -> 146
, j_2(176) -> 174
, j_2(229) -> 227
, j_2(257) -> 255
, j_2(310) -> 308
, j_2(338) -> 336
, j_2(391) -> 389
, i^#_0(2) -> 6
, i^#_0(4) -> 6
, p^#_0(2) -> 8
, p^#_0(4) -> 8
, p^#_0(10) -> 9
, p^#_1(65) -> 86
, c_1_0(9) -> 6
, c_1_1(86) -> 6
, c_5_0() -> 8
, c_5_0() -> 9
, c_5_1() -> 86}
2) {i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))}
The usable rules for this path are the following:
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))}
and weakly orienting the rules
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [8]
i^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))}
and weakly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [4]
i^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
and weakly orienting the rules
{ i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [4]
0(x1) = [1] x1 + [2]
p(x1) = [1] x1 + [1]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [8]
i^#(x1) = [1] x1 + [15]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, i^#(s(x1)) ->
c_1(p^#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ i_0(21) -> 60
, i_0(21) -> 64
, i_1(87) -> 97
, i_1(87) -> 101
, i_2(127) -> 122
, i_2(127) -> 126
, i_2(138) -> 133
, i_2(138) -> 137
, i_2(208) -> 203
, i_2(208) -> 207
, i_2(219) -> 214
, i_2(219) -> 218
, i_2(289) -> 284
, i_2(289) -> 288
, i_2(300) -> 295
, i_2(300) -> 299
, i_2(370) -> 365
, i_2(370) -> 369
, i_2(381) -> 376
, i_2(381) -> 380
, 0_0(2) -> 2
, 0_0(2) -> 15
, 0_0(2) -> 17
, 0_0(2) -> 19
, 0_0(2) -> 20
, 0_0(2) -> 21
, 0_0(2) -> 22
, 0_0(2) -> 70
, 0_0(2) -> 72
, 0_0(2) -> 74
, 0_0(2) -> 87
, 0_0(2) -> 89
, 0_0(2) -> 381
, 0_0(2) -> 383
, 0_0(2) -> 391
, 0_0(2) -> 393
, 0_0(2) -> 395
, 0_0(4) -> 2
, 0_0(4) -> 15
, 0_0(4) -> 17
, 0_0(4) -> 19
, 0_0(4) -> 20
, 0_0(4) -> 21
, 0_0(4) -> 22
, 0_0(4) -> 70
, 0_0(4) -> 72
, 0_0(4) -> 74
, 0_0(4) -> 87
, 0_0(4) -> 89
, 0_0(4) -> 381
, 0_0(4) -> 383
, 0_0(4) -> 391
, 0_0(4) -> 393
, 0_0(4) -> 395
, 0_0(21) -> 14
, 0_0(21) -> 52
, 0_0(21) -> 56
, 0_0(22) -> 20
, 0_1(82) -> 15
, 0_1(82) -> 17
, 0_1(82) -> 19
, 0_1(82) -> 20
, 0_1(82) -> 21
, 0_1(87) -> 14
, 0_1(87) -> 60
, 0_1(87) -> 64
, 0_1(87) -> 66
, 0_1(87) -> 68
, 0_1(87) -> 69
, 0_1(87) -> 91
, 0_1(87) -> 97
, 0_1(87) -> 101
, 0_1(87) -> 376
, 0_1(87) -> 380
, 0_1(87) -> 389
, 0_2(413) -> 376
, 0_2(413) -> 380
, 0_2(413) -> 389
, p_0(2) -> 15
, p_0(2) -> 17
, p_0(2) -> 19
, p_0(2) -> 20
, p_0(2) -> 21
, p_0(4) -> 15
, p_0(4) -> 17
, p_0(4) -> 19
, p_0(4) -> 20
, p_0(4) -> 21
, p_0(4) -> 22
, p_0(4) -> 70
, p_0(4) -> 72
, p_0(4) -> 74
, p_0(4) -> 87
, p_0(4) -> 89
, p_0(4) -> 381
, p_0(4) -> 383
, p_0(4) -> 391
, p_0(4) -> 393
, p_0(4) -> 395
, p_0(12) -> 11
, p_0(16) -> 15
, p_0(18) -> 15
, p_0(18) -> 17
, p_0(20) -> 15
, p_0(20) -> 17
, p_0(20) -> 19
, p_0(21) -> 20
, p_0(22) -> 15
, p_0(22) -> 17
, p_0(22) -> 19
, p_0(22) -> 20
, p_0(22) -> 21
, p_0(51) -> 14
, p_0(53) -> 14
, p_0(53) -> 52
, p_0(54) -> 53
, p_0(55) -> 14
, p_0(55) -> 52
, p_0(61) -> 60
, p_0(62) -> 61
, p_0(63) -> 60
, p_1(65) -> 60
, p_1(65) -> 64
, p_1(67) -> 14
, p_1(67) -> 60
, p_1(67) -> 64
, p_1(67) -> 66
, p_1(67) -> 69
, p_1(67) -> 91
, p_1(67) -> 97
, p_1(67) -> 101
, p_1(67) -> 376
, p_1(67) -> 380
, p_1(67) -> 389
, p_1(68) -> 376
, p_1(68) -> 380
, p_1(68) -> 389
, p_1(69) -> 389
, p_1(71) -> 70
, p_1(73) -> 70
, p_1(73) -> 72
, p_1(75) -> 70
, p_1(75) -> 72
, p_1(75) -> 74
, p_1(76) -> 75
, p_1(77) -> 76
, p_1(78) -> 77
, p_1(79) -> 76
, p_1(80) -> 75
, p_1(81) -> 70
, p_1(81) -> 72
, p_1(81) -> 74
, p_1(81) -> 87
, p_1(81) -> 89
, p_1(88) -> 87
, p_1(90) -> 14
, p_1(90) -> 69
, p_1(90) -> 97
, p_1(90) -> 101
, p_1(90) -> 376
, p_1(90) -> 380
, p_1(90) -> 389
, p_1(91) -> 376
, p_1(91) -> 380
, p_1(91) -> 389
, p_1(92) -> 14
, p_1(92) -> 69
, p_1(92) -> 91
, p_1(92) -> 97
, p_1(92) -> 101
, p_1(92) -> 376
, p_1(92) -> 380
, p_1(92) -> 389
, p_1(93) -> 92
, p_1(96) -> 97
, p_1(96) -> 101
, p_1(97) -> 376
, p_1(97) -> 380
, p_1(98) -> 97
, p_1(98) -> 101
, p_1(99) -> 98
, p_1(100) -> 97
, p_1(100) -> 101
, p_1(101) -> 376
, p_1(101) -> 380
, p_1(380) -> 389
, p_2(68) -> 389
, p_2(69) -> 389
, p_2(91) -> 389
, p_2(102) -> 97
, p_2(102) -> 101
, p_2(102) -> 376
, p_2(102) -> 380
, p_2(103) -> 376
, p_2(103) -> 380
, p_2(103) -> 389
, p_2(104) -> 97
, p_2(104) -> 101
, p_2(104) -> 103
, p_2(104) -> 376
, p_2(104) -> 380
, p_2(105) -> 376
, p_2(105) -> 380
, p_2(105) -> 389
, p_2(106) -> 389
, p_2(108) -> 107
, p_2(110) -> 107
, p_2(110) -> 109
, p_2(112) -> 107
, p_2(112) -> 109
, p_2(112) -> 111
, p_2(113) -> 112
, p_2(114) -> 113
, p_2(115) -> 114
, p_2(116) -> 113
, p_2(117) -> 112
, p_2(118) -> 107
, p_2(118) -> 109
, p_2(118) -> 111
, p_2(118) -> 127
, p_2(118) -> 129
, p_2(123) -> 122
, p_2(124) -> 123
, p_2(125) -> 122
, p_2(125) -> 126
, p_2(128) -> 127
, p_2(134) -> 133
, p_2(135) -> 134
, p_2(136) -> 133
, p_2(136) -> 137
, p_2(139) -> 138
, p_2(141) -> 138
, p_2(141) -> 140
, p_2(141) -> 148
, p_2(141) -> 150
, p_2(141) -> 152
, p_2(142) -> 122
, p_2(142) -> 126
, p_2(149) -> 148
, p_2(151) -> 148
, p_2(151) -> 150
, p_2(153) -> 148
, p_2(153) -> 150
, p_2(153) -> 152
, p_2(154) -> 153
, p_2(155) -> 154
, p_2(156) -> 155
, p_2(157) -> 154
, p_2(158) -> 153
, p_2(170) -> 133
, p_2(170) -> 137
, p_2(177) -> 176
, p_2(179) -> 176
, p_2(179) -> 178
, p_2(181) -> 176
, p_2(181) -> 178
, p_2(181) -> 180
, p_2(182) -> 181
, p_2(183) -> 182
, p_2(184) -> 183
, p_2(185) -> 182
, p_2(186) -> 181
, p_2(187) -> 176
, p_2(187) -> 178
, p_2(187) -> 180
, p_2(187) -> 208
, p_2(187) -> 210
, p_2(204) -> 203
, p_2(205) -> 204
, p_2(206) -> 203
, p_2(206) -> 207
, p_2(209) -> 208
, p_2(215) -> 214
, p_2(216) -> 215
, p_2(217) -> 214
, p_2(217) -> 218
, p_2(220) -> 219
, p_2(222) -> 219
, p_2(222) -> 221
, p_2(222) -> 229
, p_2(222) -> 231
, p_2(222) -> 233
, p_2(223) -> 203
, p_2(223) -> 207
, p_2(230) -> 229
, p_2(232) -> 229
, p_2(232) -> 231
, p_2(234) -> 229
, p_2(234) -> 231
, p_2(234) -> 233
, p_2(235) -> 234
, p_2(236) -> 235
, p_2(237) -> 236
, p_2(238) -> 235
, p_2(239) -> 234
, p_2(251) -> 214
, p_2(251) -> 218
, p_2(258) -> 257
, p_2(260) -> 257
, p_2(260) -> 259
, p_2(262) -> 257
, p_2(262) -> 259
, p_2(262) -> 261
, p_2(263) -> 262
, p_2(264) -> 263
, p_2(265) -> 264
, p_2(266) -> 263
, p_2(267) -> 262
, p_2(268) -> 257
, p_2(268) -> 259
, p_2(268) -> 261
, p_2(268) -> 289
, p_2(268) -> 291
, p_2(285) -> 284
, p_2(286) -> 285
, p_2(287) -> 284
, p_2(287) -> 288
, p_2(290) -> 289
, p_2(296) -> 295
, p_2(297) -> 296
, p_2(298) -> 295
, p_2(298) -> 299
, p_2(301) -> 300
, p_2(303) -> 300
, p_2(303) -> 302
, p_2(303) -> 310
, p_2(303) -> 312
, p_2(303) -> 314
, p_2(304) -> 284
, p_2(304) -> 288
, p_2(311) -> 310
, p_2(313) -> 310
, p_2(313) -> 312
, p_2(315) -> 310
, p_2(315) -> 312
, p_2(315) -> 314
, p_2(316) -> 315
, p_2(317) -> 316
, p_2(318) -> 317
, p_2(319) -> 316
, p_2(320) -> 315
, p_2(332) -> 295
, p_2(332) -> 299
, p_2(339) -> 338
, p_2(341) -> 338
, p_2(341) -> 340
, p_2(343) -> 338
, p_2(343) -> 340
, p_2(343) -> 342
, p_2(344) -> 343
, p_2(345) -> 344
, p_2(346) -> 345
, p_2(347) -> 344
, p_2(348) -> 343
, p_2(349) -> 338
, p_2(349) -> 340
, p_2(349) -> 342
, p_2(349) -> 370
, p_2(349) -> 372
, p_2(366) -> 365
, p_2(367) -> 366
, p_2(368) -> 365
, p_2(368) -> 369
, p_2(371) -> 370
, p_2(375) -> 376
, p_2(375) -> 380
, p_2(376) -> 389
, p_2(377) -> 376
, p_2(377) -> 380
, p_2(378) -> 377
, p_2(379) -> 376
, p_2(379) -> 380
, p_2(380) -> 389
, p_2(382) -> 381
, p_2(384) -> 381
, p_2(384) -> 383
, p_2(384) -> 391
, p_2(384) -> 393
, p_2(384) -> 395
, p_2(385) -> 365
, p_2(385) -> 369
, p_2(392) -> 391
, p_2(394) -> 391
, p_2(394) -> 393
, p_2(396) -> 391
, p_2(396) -> 393
, p_2(396) -> 395
, p_2(397) -> 396
, p_2(398) -> 397
, p_2(399) -> 398
, p_2(400) -> 397
, p_2(401) -> 396
, s_0(2) -> 4
, s_0(2) -> 15
, s_0(2) -> 17
, s_0(2) -> 19
, s_0(2) -> 20
, s_0(2) -> 21
, s_0(2) -> 22
, s_0(2) -> 70
, s_0(2) -> 72
, s_0(2) -> 74
, s_0(2) -> 87
, s_0(2) -> 89
, s_0(2) -> 381
, s_0(2) -> 383
, s_0(2) -> 391
, s_0(2) -> 393
, s_0(2) -> 395
, s_0(4) -> 4
, s_0(4) -> 15
, s_0(4) -> 17
, s_0(4) -> 19
, s_0(4) -> 20
, s_0(4) -> 21
, s_0(4) -> 22
, s_0(4) -> 70
, s_0(4) -> 72
, s_0(4) -> 74
, s_0(4) -> 87
, s_0(4) -> 89
, s_0(4) -> 381
, s_0(4) -> 383
, s_0(4) -> 391
, s_0(4) -> 393
, s_0(4) -> 395
, s_0(11) -> 10
, s_0(13) -> 12
, s_0(14) -> 11
, s_0(14) -> 13
, s_0(17) -> 16
, s_0(19) -> 18
, s_0(22) -> 2
, s_0(22) -> 15
, s_0(22) -> 17
, s_0(22) -> 19
, s_0(22) -> 20
, s_0(22) -> 21
, s_0(22) -> 22
, s_0(22) -> 70
, s_0(22) -> 72
, s_0(22) -> 74
, s_0(22) -> 87
, s_0(22) -> 89
, s_0(22) -> 381
, s_0(22) -> 383
, s_0(22) -> 391
, s_0(22) -> 393
, s_0(22) -> 395
, s_0(52) -> 51
, s_0(55) -> 54
, s_0(56) -> 53
, s_0(56) -> 55
, s_0(57) -> 14
, s_0(58) -> 57
, s_0(59) -> 58
, s_0(60) -> 59
, s_0(63) -> 62
, s_0(64) -> 61
, s_0(64) -> 63
, s_1(2) -> 75
, s_1(2) -> 81
, s_1(2) -> 338
, s_1(2) -> 340
, s_1(2) -> 342
, s_1(2) -> 370
, s_1(2) -> 372
, s_1(4) -> 75
, s_1(4) -> 81
, s_1(4) -> 338
, s_1(4) -> 340
, s_1(4) -> 342
, s_1(4) -> 370
, s_1(4) -> 372
, s_1(22) -> 75
, s_1(22) -> 81
, s_1(22) -> 338
, s_1(22) -> 340
, s_1(22) -> 342
, s_1(22) -> 370
, s_1(22) -> 372
, s_1(66) -> 65
, s_1(67) -> 93
, s_1(68) -> 67
, s_1(68) -> 92
, s_1(69) -> 14
, s_1(69) -> 60
, s_1(69) -> 64
, s_1(69) -> 66
, s_1(69) -> 68
, s_1(69) -> 69
, s_1(69) -> 91
, s_1(69) -> 97
, s_1(69) -> 101
, s_1(69) -> 376
, s_1(69) -> 380
, s_1(69) -> 389
, s_1(72) -> 71
, s_1(74) -> 73
, s_1(78) -> 85
, s_1(78) -> 176
, s_1(78) -> 178
, s_1(78) -> 180
, s_1(78) -> 208
, s_1(78) -> 210
, s_1(79) -> 78
, s_1(79) -> 219
, s_1(79) -> 221
, s_1(79) -> 229
, s_1(79) -> 231
, s_1(79) -> 233
, s_1(80) -> 77
, s_1(80) -> 79
, s_1(80) -> 257
, s_1(80) -> 259
, s_1(80) -> 261
, s_1(80) -> 289
, s_1(80) -> 291
, s_1(81) -> 76
, s_1(81) -> 80
, s_1(81) -> 300
, s_1(81) -> 302
, s_1(81) -> 310
, s_1(81) -> 312
, s_1(81) -> 314
, s_1(82) -> 75
, s_1(82) -> 81
, s_1(82) -> 338
, s_1(82) -> 340
, s_1(82) -> 342
, s_1(82) -> 370
, s_1(82) -> 372
, s_1(83) -> 70
, s_1(83) -> 72
, s_1(83) -> 74
, s_1(83) -> 82
, s_1(83) -> 87
, s_1(83) -> 89
, s_1(83) -> 381
, s_1(83) -> 383
, s_1(83) -> 391
, s_1(83) -> 393
, s_1(83) -> 395
, s_1(84) -> 83
, s_1(84) -> 107
, s_1(84) -> 109
, s_1(84) -> 111
, s_1(84) -> 127
, s_1(84) -> 129
, s_1(85) -> 84
, s_1(85) -> 138
, s_1(85) -> 140
, s_1(85) -> 148
, s_1(85) -> 150
, s_1(85) -> 152
, s_1(89) -> 88
, s_1(91) -> 90
, s_1(94) -> 14
, s_1(94) -> 69
, s_1(94) -> 376
, s_1(94) -> 380
, s_1(94) -> 389
, s_1(95) -> 94
, s_1(95) -> 389
, s_1(96) -> 95
, s_1(97) -> 96
, s_1(100) -> 99
, s_1(101) -> 98
, s_1(101) -> 100
, s_2(2) -> 384
, s_2(2) -> 396
, s_2(4) -> 384
, s_2(4) -> 396
, s_2(22) -> 384
, s_2(22) -> 396
, s_2(78) -> 222
, s_2(78) -> 234
, s_2(79) -> 262
, s_2(79) -> 268
, s_2(80) -> 303
, s_2(80) -> 315
, s_2(81) -> 343
, s_2(81) -> 349
, s_2(82) -> 384
, s_2(82) -> 396
, s_2(83) -> 112
, s_2(83) -> 118
, s_2(84) -> 141
, s_2(84) -> 153
, s_2(85) -> 181
, s_2(85) -> 187
, s_2(87) -> 420
, s_2(103) -> 102
, s_2(105) -> 104
, s_2(106) -> 97
, s_2(106) -> 101
, s_2(106) -> 103
, s_2(106) -> 105
, s_2(106) -> 376
, s_2(106) -> 380
, s_2(109) -> 108
, s_2(111) -> 110
, s_2(116) -> 115
, s_2(117) -> 114
, s_2(117) -> 116
, s_2(118) -> 113
, s_2(118) -> 117
, s_2(119) -> 69
, s_2(119) -> 376
, s_2(119) -> 380
, s_2(119) -> 389
, s_2(120) -> 119
, s_2(120) -> 389
, s_2(121) -> 120
, s_2(122) -> 121
, s_2(125) -> 124
, s_2(126) -> 123
, s_2(126) -> 125
, s_2(129) -> 128
, s_2(130) -> 106
, s_2(130) -> 376
, s_2(130) -> 380
, s_2(130) -> 389
, s_2(131) -> 130
, s_2(131) -> 389
, s_2(132) -> 131
, s_2(133) -> 132
, s_2(136) -> 135
, s_2(137) -> 134
, s_2(137) -> 136
, s_2(140) -> 139
, s_2(141) -> 154
, s_2(141) -> 158
, s_2(144) -> 142
, s_2(146) -> 122
, s_2(146) -> 126
, s_2(146) -> 144
, s_2(150) -> 149
, s_2(152) -> 151
, s_2(157) -> 156
, s_2(158) -> 155
, s_2(158) -> 157
, s_2(172) -> 170
, s_2(174) -> 133
, s_2(174) -> 137
, s_2(174) -> 172
, s_2(178) -> 177
, s_2(180) -> 179
, s_2(185) -> 184
, s_2(186) -> 183
, s_2(186) -> 185
, s_2(187) -> 182
, s_2(187) -> 186
, s_2(200) -> 146
, s_2(201) -> 200
, s_2(202) -> 201
, s_2(203) -> 202
, s_2(206) -> 205
, s_2(207) -> 204
, s_2(207) -> 206
, s_2(210) -> 209
, s_2(211) -> 174
, s_2(212) -> 211
, s_2(213) -> 212
, s_2(214) -> 213
, s_2(217) -> 216
, s_2(218) -> 215
, s_2(218) -> 217
, s_2(221) -> 220
, s_2(222) -> 235
, s_2(222) -> 239
, s_2(225) -> 223
, s_2(227) -> 203
, s_2(227) -> 207
, s_2(227) -> 225
, s_2(231) -> 230
, s_2(233) -> 232
, s_2(238) -> 237
, s_2(239) -> 236
, s_2(239) -> 238
, s_2(253) -> 251
, s_2(255) -> 214
, s_2(255) -> 218
, s_2(255) -> 253
, s_2(259) -> 258
, s_2(261) -> 260
, s_2(266) -> 265
, s_2(267) -> 264
, s_2(267) -> 266
, s_2(268) -> 263
, s_2(268) -> 267
, s_2(281) -> 227
, s_2(282) -> 281
, s_2(283) -> 282
, s_2(284) -> 283
, s_2(287) -> 286
, s_2(288) -> 285
, s_2(288) -> 287
, s_2(291) -> 290
, s_2(292) -> 255
, s_2(293) -> 292
, s_2(294) -> 293
, s_2(295) -> 294
, s_2(298) -> 297
, s_2(299) -> 296
, s_2(299) -> 298
, s_2(302) -> 301
, s_2(303) -> 316
, s_2(303) -> 320
, s_2(306) -> 304
, s_2(308) -> 284
, s_2(308) -> 288
, s_2(308) -> 306
, s_2(312) -> 311
, s_2(314) -> 313
, s_2(319) -> 318
, s_2(320) -> 317
, s_2(320) -> 319
, s_2(334) -> 332
, s_2(336) -> 295
, s_2(336) -> 299
, s_2(336) -> 334
, s_2(340) -> 339
, s_2(342) -> 341
, s_2(347) -> 346
, s_2(348) -> 345
, s_2(348) -> 347
, s_2(349) -> 344
, s_2(349) -> 348
, s_2(362) -> 308
, s_2(363) -> 362
, s_2(364) -> 363
, s_2(365) -> 364
, s_2(368) -> 367
, s_2(369) -> 366
, s_2(369) -> 368
, s_2(372) -> 371
, s_2(373) -> 336
, s_2(374) -> 373
, s_2(375) -> 374
, s_2(376) -> 375
, s_2(379) -> 378
, s_2(380) -> 377
, s_2(380) -> 379
, s_2(383) -> 382
, s_2(384) -> 397
, s_2(384) -> 401
, s_2(387) -> 385
, s_2(389) -> 365
, s_2(389) -> 369
, s_2(389) -> 387
, s_2(393) -> 392
, s_2(395) -> 394
, s_2(400) -> 399
, s_2(401) -> 398
, s_2(401) -> 400
, s_2(413) -> 420
, s_2(414) -> 413
, s_2(415) -> 414
, s_2(416) -> 415
, s_2(417) -> 416
, s_2(418) -> 417
, s_2(419) -> 418
, s_2(420) -> 419
, j_0(15) -> 14
, j_1(70) -> 69
, j_1(70) -> 376
, j_1(70) -> 380
, j_1(70) -> 389
, j_2(107) -> 106
, j_2(107) -> 376
, j_2(107) -> 380
, j_2(107) -> 389
, j_2(148) -> 146
, j_2(176) -> 174
, j_2(229) -> 227
, j_2(257) -> 255
, j_2(310) -> 308
, j_2(338) -> 336
, j_2(391) -> 389
, i^#_0(2) -> 6
, i^#_0(4) -> 6
, p^#_0(2) -> 8
, p^#_0(4) -> 8
, p^#_0(10) -> 9
, p^#_1(65) -> 86
, c_1_0(9) -> 6
, c_1_1(86) -> 6}
3) { j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_5()}
The usable rules for this path are the following:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_5()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))}
and weakly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [8]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(s(x1)) -> c_5()}
and weakly orienting the rules
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(s(x1)) -> c_5()}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [8]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [8]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{ p^#(s(x1)) -> c_5()
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [8]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [9]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
Weak Rules:
{ j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_5()
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
Weak Rules:
{ j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_5()
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ i_1(8) -> 7
, i_1(8) -> 16
, i_1(8) -> 31
, 0_0(2) -> 2
, 0_0(2) -> 8
, 0_0(2) -> 10
, 0_0(2) -> 17
, 0_0(2) -> 19
, 0_0(2) -> 21
, 0_1(8) -> 7
, 0_1(8) -> 13
, 0_1(8) -> 15
, 0_1(8) -> 16
, 0_1(8) -> 31
, p_1(4) -> 16
, p_1(4) -> 31
, p_1(5) -> 4
, p_1(9) -> 8
, p_1(11) -> 8
, p_1(11) -> 10
, p_1(12) -> 7
, p_1(12) -> 16
, p_1(12) -> 31
, p_1(14) -> 7
, p_1(14) -> 13
, p_1(14) -> 16
, p_1(14) -> 31
, p_1(18) -> 17
, p_1(20) -> 17
, p_1(20) -> 19
, p_1(22) -> 17
, p_1(22) -> 19
, p_1(22) -> 21
, p_1(23) -> 22
, p_1(24) -> 23
, p_1(25) -> 24
, p_1(30) -> 16
, p_2(6) -> 16
, p_2(6) -> 31
, p_2(11) -> 17
, p_2(11) -> 19
, p_2(11) -> 21
, p_2(26) -> 23
, p_2(27) -> 22
, s_0(2) -> 2
, s_0(2) -> 8
, s_0(2) -> 10
, s_0(2) -> 17
, s_0(2) -> 19
, s_0(2) -> 21
, s_1(2) -> 11
, s_1(2) -> 22
, s_1(6) -> 5
, s_1(7) -> 4
, s_1(7) -> 6
, s_1(10) -> 9
, s_1(11) -> 23
, s_1(11) -> 27
, s_1(13) -> 12
, s_1(15) -> 14
, s_1(16) -> 7
, s_1(16) -> 13
, s_1(16) -> 15
, s_1(16) -> 16
, s_1(16) -> 31
, s_1(19) -> 18
, s_1(21) -> 20
, s_1(26) -> 25
, s_1(27) -> 24
, s_1(27) -> 26
, s_1(28) -> 16
, s_1(29) -> 28
, s_1(30) -> 29
, s_1(31) -> 30
, j_1(17) -> 16
, p^#_0(2) -> 1
, p^#_1(4) -> 3
, j^#_0(2) -> 1
, c_3_1(3) -> 1
, c_5_0() -> 1
, c_5_1() -> 3}
4) { j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))
, p^#(s(x1)) -> c_5()}
The usable rules for this path are the following:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))
, j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_5()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p^#(s(x1)) -> c_5()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p^#(s(x1)) -> c_5()}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))}
and weakly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p^#(s(x1)) -> c_5()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p^#(s(x1)) -> c_5()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [8]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [13]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [3]
c_4(x1) = [1] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))}
Weak Rules:
{ j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p^#(s(x1)) -> c_5()}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))}
Weak Rules:
{ j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p^#(s(x1)) -> c_5()}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ i_1(8) -> 7
, i_1(8) -> 17
, i_1(8) -> 32
, 0_0(2) -> 2
, 0_0(2) -> 8
, 0_0(2) -> 10
, 0_0(2) -> 18
, 0_0(2) -> 20
, 0_0(2) -> 22
, 0_1(8) -> 7
, 0_1(8) -> 14
, 0_1(8) -> 16
, 0_1(8) -> 17
, 0_1(8) -> 32
, p_1(4) -> 17
, p_1(4) -> 32
, p_1(5) -> 4
, p_1(9) -> 8
, p_1(11) -> 8
, p_1(11) -> 10
, p_1(13) -> 7
, p_1(13) -> 17
, p_1(13) -> 32
, p_1(15) -> 7
, p_1(15) -> 14
, p_1(15) -> 17
, p_1(15) -> 32
, p_1(19) -> 18
, p_1(21) -> 18
, p_1(21) -> 20
, p_1(23) -> 18
, p_1(23) -> 20
, p_1(23) -> 22
, p_1(24) -> 23
, p_1(25) -> 24
, p_1(26) -> 25
, p_1(31) -> 17
, p_2(6) -> 17
, p_2(6) -> 32
, p_2(11) -> 18
, p_2(11) -> 20
, p_2(11) -> 22
, p_2(27) -> 24
, p_2(28) -> 23
, s_0(2) -> 2
, s_0(2) -> 8
, s_0(2) -> 10
, s_0(2) -> 18
, s_0(2) -> 20
, s_0(2) -> 22
, s_1(2) -> 11
, s_1(2) -> 23
, s_1(6) -> 5
, s_1(7) -> 4
, s_1(7) -> 6
, s_1(10) -> 9
, s_1(11) -> 24
, s_1(11) -> 28
, s_1(14) -> 13
, s_1(16) -> 15
, s_1(17) -> 7
, s_1(17) -> 14
, s_1(17) -> 16
, s_1(17) -> 17
, s_1(17) -> 32
, s_1(20) -> 19
, s_1(22) -> 21
, s_1(27) -> 26
, s_1(28) -> 25
, s_1(28) -> 27
, s_1(29) -> 17
, s_1(30) -> 29
, s_1(31) -> 30
, s_1(32) -> 31
, j_1(18) -> 17
, p^#_0(2) -> 1
, p^#_1(4) -> 3
, p^#_2(6) -> 12
, j^#_0(2) -> 1
, c_3_1(3) -> 1
, c_4_2(12) -> 3
, c_5_0() -> 1
, c_5_1() -> 3
, c_5_2() -> 12}
5) { j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))
, p^#(0(x1)) -> c_6()}
The usable rules for this path are the following:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))
, j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(0(x1)) -> c_6()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p^#(0(x1)) -> c_6()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p^#(0(x1)) -> c_6()}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))}
and weakly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p^#(0(x1)) -> c_6()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p^#(0(x1)) -> c_6()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [8]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [13]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [3]
c_4(x1) = [1] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))}
Weak Rules:
{ j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p^#(0(x1)) -> c_6()}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))}
Weak Rules:
{ j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p^#(0(x1)) -> c_6()}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ i_1(8) -> 7
, i_1(8) -> 17
, i_1(8) -> 32
, 0_0(2) -> 2
, 0_0(2) -> 8
, 0_0(2) -> 10
, 0_0(2) -> 18
, 0_0(2) -> 20
, 0_0(2) -> 22
, 0_1(8) -> 7
, 0_1(8) -> 14
, 0_1(8) -> 16
, 0_1(8) -> 17
, 0_1(8) -> 32
, p_1(4) -> 17
, p_1(4) -> 32
, p_1(5) -> 4
, p_1(9) -> 8
, p_1(11) -> 8
, p_1(11) -> 10
, p_1(13) -> 7
, p_1(13) -> 17
, p_1(13) -> 32
, p_1(15) -> 7
, p_1(15) -> 14
, p_1(15) -> 17
, p_1(15) -> 32
, p_1(19) -> 18
, p_1(21) -> 18
, p_1(21) -> 20
, p_1(23) -> 18
, p_1(23) -> 20
, p_1(23) -> 22
, p_1(24) -> 23
, p_1(25) -> 24
, p_1(26) -> 25
, p_1(31) -> 17
, p_2(6) -> 17
, p_2(6) -> 32
, p_2(11) -> 18
, p_2(11) -> 20
, p_2(11) -> 22
, p_2(27) -> 24
, p_2(28) -> 23
, s_0(2) -> 2
, s_0(2) -> 8
, s_0(2) -> 10
, s_0(2) -> 18
, s_0(2) -> 20
, s_0(2) -> 22
, s_1(2) -> 11
, s_1(2) -> 23
, s_1(6) -> 5
, s_1(7) -> 4
, s_1(7) -> 6
, s_1(10) -> 9
, s_1(11) -> 24
, s_1(11) -> 28
, s_1(14) -> 13
, s_1(16) -> 15
, s_1(17) -> 7
, s_1(17) -> 14
, s_1(17) -> 16
, s_1(17) -> 17
, s_1(17) -> 32
, s_1(20) -> 19
, s_1(22) -> 21
, s_1(27) -> 26
, s_1(28) -> 25
, s_1(28) -> 27
, s_1(29) -> 17
, s_1(30) -> 29
, s_1(31) -> 30
, s_1(32) -> 31
, j_1(18) -> 17
, p^#_0(2) -> 1
, p^#_1(4) -> 3
, p^#_2(6) -> 12
, j^#_0(2) -> 1
, c_3_1(3) -> 1
, c_4_2(12) -> 3
, c_6_0() -> 1}
6) {j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
The usable rules for this path are the following:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))}
and weakly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [8]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [8]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [9]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
Weak Rules:
{ j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
Weak Rules:
{ j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ i_1(8) -> 7
, i_1(8) -> 16
, i_1(8) -> 31
, 0_0(2) -> 2
, 0_0(2) -> 8
, 0_0(2) -> 10
, 0_0(2) -> 17
, 0_0(2) -> 19
, 0_0(2) -> 21
, 0_1(8) -> 7
, 0_1(8) -> 13
, 0_1(8) -> 15
, 0_1(8) -> 16
, 0_1(8) -> 31
, p_1(4) -> 16
, p_1(4) -> 31
, p_1(5) -> 4
, p_1(9) -> 8
, p_1(11) -> 8
, p_1(11) -> 10
, p_1(12) -> 7
, p_1(12) -> 16
, p_1(12) -> 31
, p_1(14) -> 7
, p_1(14) -> 13
, p_1(14) -> 16
, p_1(14) -> 31
, p_1(18) -> 17
, p_1(20) -> 17
, p_1(20) -> 19
, p_1(22) -> 17
, p_1(22) -> 19
, p_1(22) -> 21
, p_1(23) -> 22
, p_1(24) -> 23
, p_1(25) -> 24
, p_1(30) -> 16
, p_2(6) -> 16
, p_2(6) -> 31
, p_2(11) -> 17
, p_2(11) -> 19
, p_2(11) -> 21
, p_2(26) -> 23
, p_2(27) -> 22
, s_0(2) -> 2
, s_0(2) -> 8
, s_0(2) -> 10
, s_0(2) -> 17
, s_0(2) -> 19
, s_0(2) -> 21
, s_1(2) -> 11
, s_1(2) -> 22
, s_1(6) -> 5
, s_1(7) -> 4
, s_1(7) -> 6
, s_1(10) -> 9
, s_1(11) -> 23
, s_1(11) -> 27
, s_1(13) -> 12
, s_1(15) -> 14
, s_1(16) -> 7
, s_1(16) -> 13
, s_1(16) -> 15
, s_1(16) -> 16
, s_1(16) -> 31
, s_1(19) -> 18
, s_1(21) -> 20
, s_1(26) -> 25
, s_1(27) -> 24
, s_1(27) -> 26
, s_1(28) -> 16
, s_1(29) -> 28
, s_1(30) -> 29
, s_1(31) -> 30
, j_1(17) -> 16
, p^#_0(2) -> 1
, p^#_1(4) -> 3
, j^#_0(2) -> 1
, c_3_1(3) -> 1}
7) { j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))}
The usable rules for this path are the following:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [1] x1 + [1]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))}
and weakly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [4]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [1]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [8]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [9]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [1] x1 + [3]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))}
Weak Rules:
{ j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, p^#(p(s(x1))) -> c_4(p^#(x1))}
Weak Rules:
{ j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ i_1(8) -> 7
, i_1(8) -> 17
, i_1(8) -> 32
, 0_0(2) -> 2
, 0_0(2) -> 8
, 0_0(2) -> 10
, 0_0(2) -> 18
, 0_0(2) -> 20
, 0_0(2) -> 22
, 0_1(8) -> 7
, 0_1(8) -> 14
, 0_1(8) -> 16
, 0_1(8) -> 17
, 0_1(8) -> 32
, p_1(4) -> 17
, p_1(4) -> 32
, p_1(5) -> 4
, p_1(9) -> 8
, p_1(11) -> 8
, p_1(11) -> 10
, p_1(13) -> 7
, p_1(13) -> 17
, p_1(13) -> 32
, p_1(15) -> 7
, p_1(15) -> 14
, p_1(15) -> 17
, p_1(15) -> 32
, p_1(19) -> 18
, p_1(21) -> 18
, p_1(21) -> 20
, p_1(23) -> 18
, p_1(23) -> 20
, p_1(23) -> 22
, p_1(24) -> 23
, p_1(25) -> 24
, p_1(26) -> 25
, p_1(31) -> 17
, p_2(6) -> 17
, p_2(6) -> 32
, p_2(11) -> 18
, p_2(11) -> 20
, p_2(11) -> 22
, p_2(27) -> 24
, p_2(28) -> 23
, s_0(2) -> 2
, s_0(2) -> 8
, s_0(2) -> 10
, s_0(2) -> 18
, s_0(2) -> 20
, s_0(2) -> 22
, s_1(2) -> 11
, s_1(2) -> 23
, s_1(6) -> 5
, s_1(7) -> 4
, s_1(7) -> 6
, s_1(10) -> 9
, s_1(11) -> 24
, s_1(11) -> 28
, s_1(14) -> 13
, s_1(16) -> 15
, s_1(17) -> 7
, s_1(17) -> 14
, s_1(17) -> 16
, s_1(17) -> 17
, s_1(17) -> 32
, s_1(20) -> 19
, s_1(22) -> 21
, s_1(27) -> 26
, s_1(28) -> 25
, s_1(28) -> 27
, s_1(29) -> 17
, s_1(30) -> 29
, s_1(31) -> 30
, s_1(32) -> 31
, j_1(18) -> 17
, p^#_0(2) -> 1
, p^#_1(4) -> 3
, p^#_2(6) -> 12
, j^#_0(2) -> 1
, c_3_1(3) -> 1
, c_4_2(12) -> 3}
8) { j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(0(x1)) -> c_6()}
The usable rules for this path are the following:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
, j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))
, p^#(0(x1)) -> c_6()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [9]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, p^#(0(x1)) -> c_6()}
and weakly orienting the rules
{ i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, p^#(0(x1)) -> c_6()}
Details:
Interpretation Functions:
i(x1) = [1] x1 + [8]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [9]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
Weak Rules:
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, p^#(0(x1)) -> c_6()
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))}
Weak Rules:
{ j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
, p^#(0(x1)) -> c_6()
, i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
, i(s(x1)) ->
p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
, j^#(s(x1)) -> c_3(p^#(p(s(s(i(p(s(p(s(x1))))))))))}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ i_1(8) -> 7
, i_1(8) -> 16
, i_1(8) -> 31
, 0_0(2) -> 2
, 0_0(2) -> 8
, 0_0(2) -> 10
, 0_0(2) -> 17
, 0_0(2) -> 19
, 0_0(2) -> 21
, 0_1(8) -> 7
, 0_1(8) -> 13
, 0_1(8) -> 15
, 0_1(8) -> 16
, 0_1(8) -> 31
, p_1(4) -> 16
, p_1(4) -> 31
, p_1(5) -> 4
, p_1(9) -> 8
, p_1(11) -> 8
, p_1(11) -> 10
, p_1(12) -> 7
, p_1(12) -> 16
, p_1(12) -> 31
, p_1(14) -> 7
, p_1(14) -> 13
, p_1(14) -> 16
, p_1(14) -> 31
, p_1(18) -> 17
, p_1(20) -> 17
, p_1(20) -> 19
, p_1(22) -> 17
, p_1(22) -> 19
, p_1(22) -> 21
, p_1(23) -> 22
, p_1(24) -> 23
, p_1(25) -> 24
, p_1(30) -> 16
, p_2(6) -> 16
, p_2(6) -> 31
, p_2(11) -> 17
, p_2(11) -> 19
, p_2(11) -> 21
, p_2(26) -> 23
, p_2(27) -> 22
, s_0(2) -> 2
, s_0(2) -> 8
, s_0(2) -> 10
, s_0(2) -> 17
, s_0(2) -> 19
, s_0(2) -> 21
, s_1(2) -> 11
, s_1(2) -> 22
, s_1(6) -> 5
, s_1(7) -> 4
, s_1(7) -> 6
, s_1(10) -> 9
, s_1(11) -> 23
, s_1(11) -> 27
, s_1(13) -> 12
, s_1(15) -> 14
, s_1(16) -> 7
, s_1(16) -> 13
, s_1(16) -> 15
, s_1(16) -> 16
, s_1(16) -> 31
, s_1(19) -> 18
, s_1(21) -> 20
, s_1(26) -> 25
, s_1(27) -> 24
, s_1(27) -> 26
, s_1(28) -> 16
, s_1(29) -> 28
, s_1(30) -> 29
, s_1(31) -> 30
, j_1(17) -> 16
, p^#_0(2) -> 1
, p^#_1(4) -> 3
, j^#_0(2) -> 1
, c_3_1(3) -> 1
, c_6_0() -> 1}
9) { j^#(0(x1)) -> c_2(p^#(s(p(p(s(s(0(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_5()}
The usable rules for this path are the following:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
i(x1) = [0] x1 + [0]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
s(x1) = [1] x1 + [0]
j(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {p^#(s(x1)) -> c_5()}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j^#(0(x1)) -> c_2(p^#(s(p(p(s(s(0(p(s(p(s(x1))))))))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{p^#(s(x1)) -> c_5()}
and weakly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j^#(0(x1)) -> c_2(p^#(s(p(p(s(s(0(p(s(p(s(x1))))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(s(x1)) -> c_5()}
Details:
Interpretation Functions:
i(x1) = [0] x1 + [0]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ p^#(s(x1)) -> c_5()
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, j^#(0(x1)) -> c_2(p^#(s(p(p(s(s(0(p(s(p(s(x1))))))))))))}
Details:
The given problem does not contain any strict rules
10)
{j^#(0(x1)) -> c_2(p^#(s(p(p(s(s(0(p(s(p(s(x1))))))))))))}
The usable rules for this path are the following:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
i(x1) = [0] x1 + [0]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
s(x1) = [1] x1 + [0]
j(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules:
{j^#(0(x1)) -> c_2(p^#(s(p(p(s(s(0(p(s(p(s(x1))))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{j^#(0(x1)) -> c_2(p^#(s(p(p(s(s(0(p(s(p(s(x1))))))))))))}
and weakly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j^#(0(x1)) -> c_2(p^#(s(p(p(s(s(0(p(s(p(s(x1))))))))))))}
Details:
Interpretation Functions:
i(x1) = [0] x1 + [0]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ j^#(0(x1)) -> c_2(p^#(s(p(p(s(s(0(p(s(p(s(x1))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
Details:
The given problem does not contain any strict rules
11)
{ i^#(0(x1)) -> c_0(p^#(s(p(s(0(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_5()}
The usable rules for this path are the following:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
i(x1) = [0] x1 + [0]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
s(x1) = [1] x1 + [0]
j(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {p^#(s(x1)) -> c_5()}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, i^#(0(x1)) -> c_0(p^#(s(p(s(0(p(s(p(s(x1))))))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{p^#(s(x1)) -> c_5()}
and weakly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, i^#(0(x1)) -> c_0(p^#(s(p(s(0(p(s(p(s(x1))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(s(x1)) -> c_5()}
Details:
Interpretation Functions:
i(x1) = [0] x1 + [0]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [0] x1 + [0]
i^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ p^#(s(x1)) -> c_5()
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
, i^#(0(x1)) -> c_0(p^#(s(p(s(0(p(s(p(s(x1))))))))))}
Details:
The given problem does not contain any strict rules
12)
{i^#(0(x1)) -> c_0(p^#(s(p(s(0(p(s(p(s(x1))))))))))}
The usable rules for this path are the following:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
i(x1) = [0] x1 + [0]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
s(x1) = [1] x1 + [0]
j(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {i^#(0(x1)) -> c_0(p^#(s(p(s(0(p(s(p(s(x1))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{i^#(0(x1)) -> c_0(p^#(s(p(s(0(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{i^#(0(x1)) -> c_0(p^#(s(p(s(0(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
i(x1) = [0] x1 + [0]
0(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
j(x1) = [0] x1 + [0]
i^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5() = [0]
c_6() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ i^#(0(x1)) -> c_0(p^#(s(p(s(0(p(s(p(s(x1))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
Details:
The given problem does not contain any strict rules